L:MsgA List, P:(IdLnkIdTypeProp), i:Id.
(ML. ltgma-outlinks(M;i). P(ltg))  (ltgma-outlinks((L);i). P(ltg)) 

latex

Definitions	M1  M2, (x,yL.P(x;y)), M1 ||decl M2, P  Q, MsgAForm, P  Q, P & Q, x. t(x), , ma-outlinks(M;i), xL. P(x), , mk-ma, da-outlinks(da;i), (x  l), da-outlink-f(da;k), fpf-dom-list(f), mapfilter(f;P;L), l[i], Prop, x:A. B(x), A & B, x(s), map(f;as), , AB, A, False, P  Q, Id, IdLnk, ||as||, x:A. B(x), t  T, MsgA, (L)
Lemmas	msga wf, Id wf, IdLnk wf, length wf2, select wf, nat wf, ma-outlinks wf, l all wf, l all cons, ma-join-list wf, ma-outlinks-join, msga-sub-msg-form, msg-form-join-list, ma-join wf, l member wf, ma-outlinks-wf2, msg-form-join